1. Field of the Invention
This invention generally concerns methods for specifying and verifying systems having concurrently executing components and specifically concerns specification, simulation, verification, implementation and testing of concurrent and distributed systems.
2. Description of the Related Art
There are innumerable concurrent and distributed systems working and implemented each day throughout the world and, in some instances, beyond our world. Communication protocols, security protocols, embedded systems and process control systems are all examples of concurrent systems. These systems have become increasingly important to our personal lives and our society. Nearly every aspect of modern life is touched by a concurrent or distributed system multiple times each day. Our dependence on these systems makes their reliability critical. Therefore, their reliability should be insured.
There have been several industry and government studies done on the reliability and quality of commercially available software. These studies have consistently found software to be below accepted quality standards. The number of failures and xe2x80x9cbugsxe2x80x9d present in commercially available software is well above what is tolerated in other industries. The United States government and several software industry groups have begun efforts to implement quality control standards for commercial software. The greatest obstacle confronting these efforts is the lack of means to study, ascertain and correct errors within software designs and code.
Concomitantly, the design and implementation of concurrent and distributed systems have become increasingly more sophisticated and expensive. To insure these systems are being designed and implemented correctly and will perform in the manner intended without failure or error, certain computer aided software engineering (CASE) tools have been developed. CASE tools aim to ease and sometimes automate the process of software development.
Verification tools are a type of CASE tool that provide a means for verifying whether a planned or pre-existing system will satisfy its requirements. The use of CASE tools, and especially verification tools, can lead to the detection of errors early within the system development life cycle. The early detection of design errors will lead to money and time saved, increased quality and greater reliability and robustness of the final system.
Most existing verification tools have been designed to analyze synchronous hardware systems. Such tools, typically found in computer aided design (CAD) packages, are being routinely used in the hardware industry. However, asynchronous systems, possessing multiple independent threads of control, are becoming more prevalent. Software systems are typically asynchronous and the popularity of asynchronous hardware design is increasing. Thus, the need for verification tools for asynchronous systems is acute. This need is further accentuated since many functions originally performed in hardware are now being delegated to software systems.
Most verification tools today are severely limited in their ability to analyze these complex systems. One source of this limitation is known as the xe2x80x9cstate explosionxe2x80x9d problem. A xe2x80x9cstatexe2x80x9d in this context is a possible configuration the system can enter, or, alternatively, a snapshot of the system""s execution.
State explosion occurs because, in general, the size of a system""s state space grows exponentially in the size of the system""s description. Therefore, the analysis of systems with relatively succinct descriptions can prove intractable for even the most powerful computers available.
To overcome state explosion, partial-order reduction techniques have been developed. Partial-order reduction is made possible since some system states, and the execution paths leading to these states are, in a formal sense, redundant. These redundancies can be safely ignored without compromising verification efforts. By avoiding these redundant states during analysis, the size of the state space to be searched may be dramatically reduced.
Another technique that has been developed for overcoming state explosion is local verification. Local verification is incremental, demand driven exploration of the state space, depending on the needs of the specific verification task at hand.
Model checking is a formal verification technique based on state exploration. Model checking allows one to check whether a state-machine representation of a system is a model of, or satisfies, a formula in temporal logic. Temporal logic allows for the specification of critical system properties such as freedom from deadlock and eventual service guarantees. Temporal logic formulas can be seen as mathematically precise system requirements.
The input to a model checker is a state-machine-based specification of the system to be verified and one or more system properties expressed in temporal logic. The output is either a declaration that the property is true or an identification of a portion of the state space falsifying the property.
There are several commercial and academic version model checkers available today. These use versions of temporal logic that restrict the class of logical properties that can be expressed.
Software designed to analyze and generate concurrent and distributed systems is herein disclosed. The invention""s preferred embodiment comprises specification, simulation, verification, and code-generation capabilities.
For specification, the invention comprises graphical and textual editors. In the preferred embodiment, these allow one to render systems in GCCS and VPL. GCCS is a graphical coordination language for specifying hierarchically structured systems of communicating state machines. The GCCS network editor allows users to define the communication topology of their system in terms of nodes and communication links. Each node represents a system (network), and systems may be composed of sub-systems, sub-systems may be composed of sub-sub-systems, and so on. At the lowest level of a GCCS hierarchy are processes. The graphical process editor supports the creation of state machines. Users may also create networks and processes using VPL.
Two distinguishing aspects of GCCS and its realization via the network and process editors are: (1) GCCS has a formal xe2x80x9coperational semanticsxe2x80x9d that allows GCCS-based specifications to be simulated and analyzed in mathematically precise ways; (2) GCCS is a true coordination language in the sense that any notation for processes with a suitable operational semantics could be used for defining processes.
VPL stands for xe2x80x9cvalue passing languagexe2x80x9d. It is a textual specification language used to define system components that exchange data values and that exhibit complex control structure. The invention contains a VPL editor that allows users to input VPL descriptions in a structure-based way. The VPL editor also performs static type checking to ensure that the right kinds of values are communicated in all contexts. Like GCCS, VPL is equipped with a formal operational semantics.
The graphical/textual combination is extremely useful in practice. In system design, some aspects (e.g. system architecture) are best captured graphically, while others (e.g. complex data and control structures) are easier to express textually. This improves the efficiency of system designers and maintainers.
Preferably, each editor comprises a structure-based editor and static type checker. The structure-based editor guarantees that one""s input is syntactically correct. The static type checker insures that all data is used in a sound and complete manner.
The specification tools of this invention support open system specifications and support the analysis of subsystems independently of other subsystems. These tools can describe and analyze system components without specifying the entire system. These tools overcome what has been necessary, closed-world assumptions made by other specification tools. Since GCCS is able to combine systems or subsystems together into a unified whole regardless of the language used to describe the subsystems, it becomes the glue for assembling subsystems into systems. The specification element of the invention can therefore support hierarchically structured system designs which is the natural form for software to be composed.
The simulation element of the invention is based on the formal semantics of the specification languages. Simulation must always be faithful to the formal model which is insured in the invention. Since the invention is targeted at the analysis of hierarchical systems, it can simulate different levels of subsystems simultaneously.
The simulation element of the invention is a highly graphical and interactive system simulator, providing many forms of simulation output to the user. The simulator allows users to step through the execution of their designs one execution step at a time. They may also set break points and let the system run autonomously until a break point is reached. In this regard, the simulator functions like a traditional debugger from programming languages.
The simulator also supports replay, history lists, message sequence charts (MSCs) and reverse execution. History lists allow a user to restart a simulation at any point in the history of the simulation. MSCs provide a visually appealing depiction of process interactions, such as inter-process synchronizations and communications. Both graphical and textual specifications can be simulated in the manner just described.
The third element of the invention is the means for verification. This preferably includes model checking, equivalence checking, minimization and preorder checking. Model checking is used to decide if a system satisfies a temporal-logic formula. Equivalence checking is the process of determining whether two systems are equivalent to each other according to some mathematically defined notion of equivalence. Minimization refers to the process of reducing a system""s state space by collapsing blocks of equivalent states into single states. Preorder checking is aimed at determining if one system refines or implements another system according to some mathematically defined refinement ordering. Collectively, these methods are a powerful machinery for manipulating and reasoning about formal system designs.
Computationally, a key aspect of the invention""s model checking is that the entire procedure is fully automatic when the system to be analyzed is finite-state, i.e. the state space comprises a finite, albeit potentially large, number of system states. This is the case for many practical applications, such as embedded system or control software. When this is not the case, mathematically defined abstractions are applied to the system to render it finite. The advantage of an automatic verification technique is that the user need not interact with the model checker while it executes.
In one embodiment, the property specification language of the model checker is the modal mu calculus, a highly expressive temporal logic. Virtually every temporal logic used by existing model checkers can be reduced to the modal mu-calculus, meaning that the mu-calculus is more expressive than these logics. Besides being able to express standard system requirements such as deadlock freedom, the mu-calculus can describe subtle system correctness properties. One example of these correctness properties is possibility properties which are of the form: it is always possible to find an execution path along which a certain designated event occurs.
The model checker of the invention uses a new kind of partial-order reduction method to eliminate redundant portions of the state space from analysis. The technique is the first of its kind to be targeted for use with the modal mu-calculus. Like other partial-order methods, it uses an xe2x80x9cindependence checkxe2x80x9d to identify redundant system states and transitions. However, unlike previously proposed techniques, this partial-order method requires no information about the semantics of transitions. In particular, there is no need to associate transitions with source-level program operations, and no need to provide an independence relation among operations. Moreover, the notion of independence is a dynamic one and not, as in previous approaches, fixed in advance. Dynamic information regarding the behavior of the specification is used to determine independence.
The model checker is also local. That is, given a system S and a modal mu calculus formula f, the model checker explores only the portion of S""s state space that is necessary to determine if S satisfies f. Experience has shown that this explored portion can be dramatically smaller than S""s entire state space, and local model checking represents a very practical approach to verification.
The model checker supports the analysis of open systems, i.e., subsystems can be verified independently of one another. In contrast, other model checkers require that all system components be present before analysis can be carried out. The ability to handle open systems stems from the fact that the operational semantics used for the design languages is based on process algebra, a specification formalism for open systems. The ability to accommodate open systems allows for a much more flexible system design process.
The verification element also performs equivalence checking, the process of determining if two systems exhibit identical observable behavior. Equivalence checking can be used to check if a system design conforms to its high-level xe2x80x9cservice specificationxe2x80x9d. For example, if the observable behavior of a communications protocol is identical to that of a perfect communication channel that delivers all messages in order, then it would be justifiable to deem the protocol correct.
Equivalence checking also provides the basis for performing state minimization. By collapsing blocks of equivalent system states into single states, one can obtain the smallest possible state space that still exhibits the same observable behavior as the original system. Like partial-order reduction, this technique is used to eliminate redundant and unnecessary portions of the state space from consideration during analysis. In combination with the invention""s capability to handle open systems, minimization becomes even more potent. That is, system components can be added one at a time to the analysis, performing state minization each step of the way.
Lastly, the verification element of the invention performs preorder checking. Preorder checking determines whether one system is a refinement of another, or, in more practical terms, whether one system implements another. Preorder checking is used in a fashion analogous to equivalence checking but is more appropriate when one is dealing with system specifications given at different levels of abstraction.
The fourth element of the invention is its capability to generate executable code from system designs. The code generators relieve the user of the burden of having to manually recode their designs in the target language of the implemented system. They also eliminate the possibility of errors in the translation process. The generated code implements the state machines and the communication infrastructure. It also includes hooks for user-supplied code.
The code-generation element of the invention includes a novel solution to the xe2x80x9cinput/output guard scheduling problemxe2x80x9d. This is the problem of avoiding deadlocks that can arise when processes are allowed to choose nondeterministically to perform an input or output operation to a potential communication partner. The invention""s solution is targeted toward hierarchically structured networks of processes and introduces a xe2x80x9ccommunications schedulerxe2x80x9d at each level of the hierarchy to properly arbitrate requests for input and output emanating from lower levels of the hierarchy. This solution is more efficient than a strictly centralized solution in which only a single, system-wide scheduler is deployed, and, at the same time, avoids delegating too much authority to individual processes (which could lead to deadlock).
The entire invention is based upon the existence of an underlying formal model of system behavior, namely, operational semantics. Operational semantics mathematically and unambiguously defines the step-by-step execution behavior of a system or subsystem, and all specifications rendered in the invention are equipped xe2x80x9cfor freexe2x80x9d with such a semantics. The invention""s model checker, equivalence checker, minimizer, preorder checker, and simulators, all rely on operational semantics to ensure that these activities are carried out faithfully; i.e., without the possibility of error due to the introduction of spurious system behaviors or the accidental elimination of actual system behaviors.